Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Pullback properties #449

Merged
merged 5 commits into from
Feb 20, 2025
Merged

Pullback properties #449

merged 5 commits into from
Feb 20, 2025

Conversation

frederikgebert
Copy link

I proved the pasting law for pullbacks and added it to Pullback/Properties.agda.
I'm new to agda, so any feedback is much appreciated. I hope this fits into this library!

JacquesCarette
JacquesCarette requested changes Feb 6, 2025
View reviewed changes
Copy link
Collaborator

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is generally very nice. Just a few minor comments.

There might be a second round, as some thing might become more obvious once these clean-ups are down.

@frederikgebert
Copy link
Author

Thank you for your feedback. I removed all implicit arguments and everything still works. I'm very impressed by Agda's ability to fill in those arguments! I also implemented the other changes you proposed. Everything is so much cleaner now.. :O
I will go through the proof again in the next days to see if I can shorten it by removing unnecessary definitions.

@JacquesCarette
Copy link
Collaborator

Don't go overboard on shortening. Sometimes some intermediate definitions are useful for conceptual clarity. But in general, yes, shorter is better.

Move intermediate equations to definitions that use them.
7d87911 
Increases clarity because:
- the intermediate equations are only relevant in the context of the definition that uses them.
- the type declaration of intermediate equations is much shorter.
@frederikgebert
Copy link
Author

I removed some definitions that seemed redundant and moved intermediate equations to the definitions that use them. This increases clarity because the typing judgements are much shorter.
I also removed some lines by using pull, push and extend reasoning.
Sorry for basically rewriting the whole proof but I think it makes more sense now.

@JacquesCarette JacquesCarette merged commit 8509bc5 into agda:master Feb 20, 2025
1 check passed
@frederikgebert frederikgebert deleted the pullback-properties branch February 21, 2025 11:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JacquesCarette JacquesCarette JacquesCarette approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@frederikgebert @JacquesCarette